\documentclass[a4paper,10pt]{article}

\usepackage{amsfonts, amsmath, amsthm, amssymb}
\usepackage[english]{babel}
%\usepackage{bookman}
%\usepackage{pxfonts}

%\usepackage[T1]{fontenc}
\usepackage{subfig}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{a4wide}
\pagestyle{headings}
\pagestyle{plain}
\usepackage{hyperref}

\usepackage{moreverb}
\usepackage{epstopdf}


\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}

\newcommand{\mint}[1]{\;\mathrm{#1}}
\newcommand{\then}{\Rightarrow}

\newcommand{\w}{\mathbf{w}}
\renewcommand{\c}{\mathbf{c}}
\newcommand{\1}{\mathbf{1}}


%\frenchspacing

\title{Automatic reasoning 4\\ Filling the Grid}
\author{Niklas Weber \\ 0841420, \\ Matúš Tejiščák \\ 4176200}
\date{\today}

\begin{document}

\maketitle

\section{The problem}
In this task we look at a $18*12$ grid on which squares are being laid out. There always are one $7*7$, one $6*6$, two $5*5$ and three $4*4$ squares. The question is: How many $3*3$ squares can possibly fit in addition to the other parts?
\section{Representation of the model}
Intuitively, an upper boundary on this number can be established if the space could be used fully:
\[(18*12 - 7^2  - 6^2 - 2*5^2 - 3*4^2) / 3^2 \approx 3.67\]
Thus $3$ is the highest possible outcome, which supplies us with a first check of our implementation.
For the creation of a model we shall look at the generalized problem of a $m*n$ grid. Let furthermore $s = (s_1,s_2,s_3,...,s_n)$ be a vector, where $s_a$ is the size of a side of part $x$\footnote{N.B.: With 'parts' I mean the squares to be placed on the grid. As this is the nomenclature also used in the implementation it might be helpful to also use it in the model.}. This vector is known. As we shall later increase the number of parts in a stepwise manner to find the maximal satisfiable configuration it is a handy convention to say that the lower part numbers are reserved for the invariable parts. For our concrete instance of the problem this means: $s_1$ up to $s_7$ represent the given parts, everything above is one of the $3*3$ squares.

Let us now look at the variable part of this satisfiability question: the position of the parts. Let $p = (p_1,p_2,p_3,...,p_n)$ be a vector and $p_a$ be a tuple $(x_a,y_a)$, being the $x$ and $y$ coordinates for part $a$\footnote{Note the reverse order when compared to the $m*n$-notation used for matrices. It holds that $1 \leq x \leq n$ and $1 \leq y \leq m$}. The actual task now consists of two parts:
\begin{enumerate}
\item Pick a number $c$ of $3*3$ squares
\item Find out whether there are positions for the $7+c$ parts to be placed which abide by two constraints:
\begin{enumerate}
	\item Every part is placed inside of the boundaries of the grid
	\item No two parts overlap
\end{enumerate}
\end{enumerate}
The first part is what we shall do by hand (and, knowing that in this specific case there can be no solution greater than $c = 3$, this is quite feasible). The satisfiability of the constraints shall be checked automatically. Accordingly, we have to make them more precise. Let us thus now focus on their formalization.
\paragraph{Every part is placed inside of the boundaries of the grid:}
The right border of a part is given by starting position plus size of one side minus one\footnote{One might note that one unit of size is 'taken up' by filling the initial field. Furthermore it should be noticed that $(1,1)$ in our interpretation means the upper left field of the grid. To see an example for a possible grid see the solution further below.}. In terms of the original vectors:
\[a_{rBorder} = x_a + s_a - 1\]
The lower border is given likewise:
\[a_{lBorder} = y_a + s_a - 1\]
The constraint can now be expressed rather simply. Let $P$ be the set of parts. Then:
\begin{align*}
	\forall p \in P:&\\
	& x_p \geq 0~\wedge\\
	& y_p \geq 0 ~\wedge\\
	& x_p + s_p - 1\leq n ~\wedge\\
	& y_p + s_p - 1\leq m
\end{align*}
\paragraph{No two parts overlap:}
First, we make a simple observation: two parts do not overlap if a) one part is strictly higher than the other (meaning: its lower boundary is higher than the upper boundary of the second part) or b) one part is strictly more left than the other or c) both. We can express this as follows:\\
\begin{align*}
	\forall p_0, p_1 \in P: p_0 \neq p_1 \Rightarrow &\\
	& ((x_{p_0} < x_{p_1} \wedge x_{p_0} + s_{p_0} \leq x_{p_1}) ~\vee & \text{($p_0$ further left)}\\
	& (x_{p_1} < x_{p_0} \wedge x_{p_1} + s_{p_1} \leq x_{p_0})) & \text{($p_1$ further left)} \\
	& \vee\\
	& ((y_{p_0} < y_{p_1} \wedge y_{p_0} + s_{p_0} \leq y_{p_1}) ~\vee & \text{($p_0$ further down)}\\
	& (y_{p_1} < y_{p_0} \wedge y_{p_1} + s_{p_1} \leq y_{p_0})) & \text{($p_1$ further down)} 
\end{align*}
\section{Implementation}
We have implemented this problem as a Yices program, using its specification language\footnote{\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/task4.ys}}.
The number of $3*3$ parts can be freely chosen by changing one constant definition. To find our solution we start at 3 and lower this value until the either we have reached 0 or the formula becomes satisfiable.\\
The variable part of this problem (the positions of the individual parts) is implemented as an empty function:
\begin{verbatimtab}
(define part-position :: (-> nat pos))
\end{verbatimtab}
This can be read as: part-position is a function which, given a natural number, returns a position. The natural number in question is the index of part, ranging from 0 to 6 plus the number of $3*3$ squares. Please note that this diverges from the model given above, as now we start counting at 0. This also holds true for the position in the grid ($(0,0)$ being the upper left corner). The constraints now form constraints on the interpretation of this empty function.
The \textbf{first constraint} (positioned inside of the boundaries) is expressed as the following function:
\begin{verbatimtab}[4]
(define part-inside-boundaries :: (-> pos dim bool)
	(lambda (p::pos d::dim)
		(and  
			(<= (+ (select p x) (select d x)) 12)
			(<= (+ (select p y) (select d y)) 18) 
			(>= (select p x) 0) 
			(>= (select p y) 0) 
		)
	)
)
\end{verbatimtab}
This function is called for every part's position. Note here, that 11 and 17 are the original boundaries. 12 and 18 already include an added $+1$. This is an equivalent way of writing the original inequality from our model.

The \textbf{second constraint} (no overlap) has been implemented as follows:
\begin{verbatimtab}[4]
(define parts-do-not-overlap :: (-> pos dim pos dim bool)
	(lambda (p0::pos d0::dim p1::pos d1::dim)
		(or 
			(or 
				(and 
					(< (select p0 x) (select p1 x)) 
					(<= (+ (select p0 x) (select d0 x)) (select p1 x))
				) 
				(and 
					(< (select p1 x) (select p0 x)) 
					(<= (+ (select p1 x) (select d1 x)) (select p0 x))
				)
			)

			(or 
				(and 
					(< (select p0 y) (select p1 y))
					(<= (+ (select p0 y) (select d0 y)) (select p1 y))
				)
				(and 
					(< (select p1 y) (select p0 y)) 
					(<= (+ (select p1 y) (select d1 y)) (select p0 y))
				)
			)
		)
	)
)
\end{verbatimtab}
When comparing with the section above it can be seen that this is a direct translation of the original constraint. A minor modification: whether the two parts being tested for non-overlap are not identical is checked on a higher layer in the code. As this is trivial we shall omit it here.\\
The rest of the code is mainly bookkeeping, e. g. calling the no-overlap function for every pair of squares and setting up the logical context.
\section{Solution}
Using the method and implementation described above we have found the maximal number of $3*3$ squares for which the formula is satisfiable to be 2. A satisfying assignment is:
\begin{verbatim}
(= (part-position 0) (mk-record x::1 y::0))
(= (part-position 1) (mk-record x::6 y::12))
(= (part-position 2) (mk-record x::3 y::7))
(= (part-position 3) (mk-record x::1 y::13))
(= (part-position 4) (mk-record x::8 y::8))
(= (part-position 5) (mk-record x::8 y::4))
(= (part-position 6) (mk-record x::8 y::0))
(= (part-position 7) (mk-record x::0 y::10))
(= (part-position 8) (mk-record x::0 y::7))
\end{verbatim}
A visualization of this solution:
\begin{figure}[htp]
	\begin{center}
		\includegraphics[width=0.5\textwidth]{task3-viz1}
		%\includegraphics[width=0.5\textwidth]{task2-selected}
	\end{center}
	\caption{A solution to the problem found by Yices}
	\label{fig:sol-1}
\end{figure}


\end{document}
